The use of assertions
The use of assertions
Overview
Overview
◼ Perhaps the most critical general property of an element is its grade. In GrassmannAlgebra you can declare a symbol to be a scalar symbol (in which case it has grade 0), or a vector symbol (in which case it has grade 1). You can also specify a graded element by writing its grade as an underscript to the symbol. For example is interpreted by GrassmannAlgebra to be of grade
α
m
m
. Each of these mechanisms for specifying grade are global mechanisms, valid no matter which GrassmannAlgebra functions are being used.◼ GrassmannAlgebra also has a local mechanism for asserting the grade of a symbol. Wherever it makes sense, a function can take further arguments which assert symbols to have certain grades. In particular, functions associated with the computation or testing of grades and the simplification of expressions can take grade assertions as arguments. These assertions are used only by that function during that particular application of it.
◼ The syntax is uniformly of the form GradeOrTransformationFunction[X,A], or GradeOrTransformationFunction[X,T,A], where X is a Grassmann expression (or list of Grassmann expressions) and A is a sequence of grade assertions.
◼ A grade assertion is of the form or , where
x∈
★Λ
m
{x,y,z,…}∈
★Λ
m
x
, y
, z
, …
are the symbols whose grades are being asserted, and m
is the grade. The grade m
can be a list of grades if the symbol whose grade is being asserted is multigraded.◼ A grade assertion may also be a composite grade assertion. A composite grade assertion takes the form Assertions L, where L is a list of grade assertions. This mechanism allows lists of assertions to be provided as arguments to a function in a way additional to its listability behaviour. For example:
 | Assertions |
★Λ
m
★Λ
m
◼ The symbol ∈ in the assertion expression can be entered with el, ★ with *5 and Λ with L.
◼ You can assert the grades of any symbols, whether they already have a declared grade (for example, scalar symbols or vector symbols), or whether they are completely new symbols.
◼ You can use simple expressions as symbols in your assertions, for example, subscripted or superscripted symbols (, ); or symbols with other heads, (f[x]).
x
i
i
x
◼ You can use assertions to check the grades of symbols that already have a declared grade, for example scalar symbols or vector symbols. If the declared grade and the asserted grade are the same, the assertion will return True. If they are not, the assertion will be returned unevaluated.
★A;a∈,x∈,x∈,Z∈
★Λ
0
★Λ
1
★Λ
0
★Λ
0
If you use the form which asserts the grade of a list of symbols, any symbols which already have that grade declared will be eliminated, and any remaining symbols will be output using Mathematica's "alternative" form. If all the symbols in the list have the asserted grade, the result will yield .
{a}∈,{a,b,c}∈,{x,Y,Z}∈,{x,Y,Z}∈
★Λ
0
★Λ
0
★Λ
1
★Λ
2
◼ Any number of assertions of this form can be made in a sequence following the expression given as first argument. The effect is that all of the assertions will be accepted by the function in carrying out its operation. If F is the name of the grade or simplification function and are grade assertions which are all to hold simultaneously, the syntax is thus
A
i
F[X,,,…]
A
1
A
2
◼ Each GradeOrTransformationFunction is listable which permits the making of lists of expressions and assertions . However, these follow Mathematica's rules for listable functions of several arguments. In particular, if F is the name of the grade or simplification function
A
i
F[X,{,,…}]⟶{F[X,],F[X,],…}
A
1
A
2
A
1
A
2
F[{,,…},A]⟶{F[,A],F[,A],…}
X
1
X
2
X
1
X
2
The following will also work providing there is exactly one assertion per expression.
F[{,,…},{,,…}]⟶{F[,],F[,],…}
X
1
X
2
A
1
A
2
X
1
A
1
X
2
A
2
A list of assertions can be provided to work with each of the expressions in a list by using the option.
F{,,…},
{,,…}⟶{F[,,,…],F[,,,…],…}
X
1
X
2
 | Assertions |
A
1
A
2
X
1
A
1
A
2
X
2
A
1
A
2
Examples
Examples
◼ We begin the following examples by declaring a 4-space.
★A;
;
 | ★ℬ |
4
◼ The simplest case is that of a single expression, for example x⋀x. By default x is a vector symbol of grade 1, hence x⋀x is of grade 2, but simplifies to zero.
Grade[x⋀x]
2
| ★ |
0
If, now, we include the assertion
A
that x
is a 2-element, we find that x⋀x
is of grade 4, and does not simplify (necessarily) to zeroA=x∈;Grade[x⋀x,A]
★Λ
2
4
| ★ |
x⋀x
Note that these assertions are local to the functions and (
★
). They do not change the global nature of the symbol x
. It is still a vector symbol of grade 1.
[x],Grade[x]
 | VectorSymbolQ |
{True,1}
◼ We now take a slightly more complex expression. In the global environment X is of grade 3 since its component symbols are all vector symbols.
Grade[x⋀y⋀z]
3
To assert different grades for
x
, y
, and z
, we can include the assertions as extra arguments.Gradex⋀y⋀z,x∈,y∈,z∈
★Λ
0
★Λ
2
★Λ
2
4
◼ If we give conflicting assertions, it is the first one (of the conflicting cases) in the union of the assertions that takes effect. In the next example, the of the assertions places first in the list, and hence it is this one that is applied. Normally this feature means that an assertion of lower grade will take precedence over one of higher grade. But care must be taken when symbolic grades are used.
x∈
★Λ
2
Gradex,x∈,x∈,x∈
★Λ
3
★Λ
4
★Λ
2
◼ The GrassmannAlgebra functions that are meaningful with assertions are also . Hence if we enclose the sequence of assertions in a list, we find that the function has been applied to the one expression as many times as there are assertions. In this example, there are thus 4 results.
Gradex,x∈,x∈,x∈
★Λ
3
★Λ
4
★Λ
2
{3,4,2}
◼ On the other hand, if the function is applied to a list of expressions, all the assertions are applied to each expression in turn. In this example there are thus 4 results.
| ★ |
x⋀Y
★Λ
0
★Λ
m
,xy,0,xY
2
x
(4-m)m
(-1)
◼ The listability of the grade and simplification functions means that applying a list of assertions to a list of expressions of equal length results in each assertion being applied only to the expression in the corresponding position in the list of expressions. In the following example there are a list of 3 expressions and a list of 3 assertions, leading to a list of 3 results.
Clear[X,Y,Z];Grade{X,Y,Z},X∈,Y∈,Z∈
★Λ
1
★Λ
2
★Λ
3
{1,2,3}
◼ The situation may arise however, that you wish to make a composite assertion whose length does not conform to Mathematica's listability behaviour. In this case you can collect assertions and make them into a single composite assertion by using the option. Composite assertions behave like sequences of assertions.
| ★ℬ |
6
| Assertions |
★Λ
1
★Λ
2
★Λ
3
{3,5}
The option can take nested lists of assertions. Such nested lists of assertions are effectively flattened.
Grade{X⋀Y,Y⋀Z,V⋀W},
X∈,Y∈,Z∈,W∈,V∈
| Assertions |
★Λ
1
★Λ
2
★Λ
3
★Λ
3
★Λ
m
{3,5,3+m}
Grade or transformation functions which can take assertions
Grade or transformation functions which can take assertions
◼ Functions associated with the computation or testing of grades or the transformation of expressions, which can take assertions as extra arguments are , , , , , , , , , , , , , , , , , , , , , , , , , , , , , , , , .
 |
|
""